\begin{tabbing}
$\forall$\=${\it es}$:ES, $k$:Knd, $T$:Type, $l$:IdLnk, ${\it ds}$, ${\it dt}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]$g$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$(${\it dt}$(${\it tg}$)?Void List))) List.
\-\\[0ex]sends $k$(v:$T$) on $l$:tagged($g$,State(${\it ds}$),v):${\it dt}$ $\in$ Prop
\end{tabbing}